package river_city_ransom.contracts;

import exceptions.ComposantError;
import exceptions.InvariantError;
import exceptions.PostconditionError;
import exceptions.PreconditionError;
import river_city_ransom.services.Equipable;
import river_city_ransom.services.Personnage;
import river_city_ransom.services.Position;
import tools.Toolbox;


public class Personnage_C extends Equipable_C implements Personnage {
	public Personnage_C(Personnage delegate) {
		super(delegate);
	}
	
	@Override
	protected Personnage delegate() {
		return (Personnage) super.delegate();
	}
	
	/** __________________________________________________________ INVARIANTS */
	public void checkInvariants() throws ComposantError {
		super.checkInvariants();
		
		boolean inv;
//		inv estEquipable(P) = estGele(P) > 0
		inv = estEquipable() == (estGele() > 0);
		if(!inv) {
			throw new InvariantError("estEquipable(P) = estGele(P) > 0");
		}
//		inv (estPorte(P) v estJete(P) != 0) -> estGele(P) > 0
		if(estPorte() || estJete() != 0) {
			inv = estGele() > 0;
			if(!inv) {
				throw new InvariantError("(estPorte(P) v estJete(P) != 0) -> estGele(P) > 0");
			}
		}
//		inv pointsDeVie(P) <= maxPointsDeVie(P)
		inv = pointsDeVie() <= maxPointsDeVie();
		if(!inv) {
			throw new InvariantError("pointsDeVie(P) <= maxPointsDeVie(P)");
		}
//		inv estVaincu(P) = pointsDeVie(P) <= 0
		inv = estVaincu() == (pointsDeVie() <= 0);
		if(!inv) {
			throw new InvariantError("estVaincu(P) = pointsDeVie(P) <= 0");
		}
//		inv estEquipe(P) = choseEquipee(P) != NULL
		inv = estEquipe() == (choseEquipee() != null);
		if(!inv) {
			throw new InvariantError("estEquipe(P) = choseEquipee(P) != NULL");
		}
//		inv estGele(P) >= 0
		inv = estGele() >= 0;
		if(!inv) {
			throw new InvariantError("estGele(P) >= 0");
		}
	}
	
	/** _________________________________________________________ OBSERVATORS */
	@Override
	public String nom() {
		return delegate().nom();
	}
	
	@Override
	public int force() {
		return delegate().force();
	}

	@Override
	public int maxPointsDeVie() {
		return delegate().maxPointsDeVie();
	}

	@Override
	public int pointsDeVie() {
		return delegate().pointsDeVie();
	}

	@Override
	public boolean estVaincu() {
		return delegate().estVaincu();
	}

	@Override
	public Equipable choseEquipee() {
		return delegate().choseEquipee();
	}

	@Override
	public boolean estEquipe() {
		return delegate().estEquipe();
	}

	@Override
	public int estGele() {
		return delegate().estGele();
	}
	
	@Override
	public boolean versLaDroite() {
		return delegate().versLaDroite();
	}

	/** ___________________________________________________________ OPERATORS */
	@Override
	public void deposerPointsDeVie(int pv) throws ComposantError {
		boolean pre;
//		pre deposerPointsDeVie(P, pv) require estGele(P) = 0 ^ pv > 0
		pre = estGele() == 0 && pv > 0;
		if(!pre) {
			throw new PreconditionError("deposerPointsDeVie(P, pv) require estGele(P) = 0 ^ pv > 0");
		}
		
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		int mpv_pre = maxPointsDeVie();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();
		
		checkInvariants();
		
		delegate().deposerPointsDeVie(pv);
		
		checkInvariants();
		
		boolean post;
//		post pointsDeVie(deposerPointsDeVie(P, pv)) = min(pointsDeVie(P) + pv, maxPointsDeVie(P))
		post = pointsDeVie() == Math.min(pv_pre + pv, mpv_pre);
		if(!post) {
			throw new PostconditionError("pointsDeVie(deposerPointsDeVie(P, pv)) = min(pointsDeVie(P) + pv, maxPointsDeVie(P))");
		}
//		post estPorte(deposerPointsDeVie(P, pv)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(deposerPointsDeVie(P, pv)) = estPorte(P)");
		}
//		post estJete(deposerPointsDeVie(P, pv)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(deposerPointsDeVie(P, pv)) = estJete(P)");
		}
//		post choseEquipee(deposerPointsDeVie(P, pv)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(deposerPointsDeVie(P, pv)) = choseEquipee(P)");
		}
//		post position(deposerPointsDeVie(P, pv)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(deposerPointsDeVie(P, pv)) = position(P)");
		}
//		post versLaDroite(deposerPointsDeVie(P, pv)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(deposerPointsDeVie(P, pv)) = versLaDroite(P)");
		}
//		post estGele(deposerPointsDeVie(P, pv)) = estGele(P)
		post = eg_pre == estGele();
		if(!post) {
			throw new PostconditionError("estGele(deposerPointsDeVie(P, pv)) = estGele(P)");
		}
	}

	@Override
	public void retirerPointsDeVie(int pv) throws ComposantError {
		boolean pre;
//		pre retirerPointsDeVie(P, pv) require !estVaincu(P) ^ pv > 0
		pre = !estVaincu() && pv > 0;
		if(!pre) {
			throw new PreconditionError("retirerPointsDeVie(P, pv) require !estVaincu(P) ^ pv > 0");
		}
		
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Equipable ce_pre = choseEquipee();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();
		
		checkInvariants();
		
		delegate().retirerPointsDeVie(pv);
		
		checkInvariants();
		
		boolean post;
//		post pointsDeVie(retirerPointsDeVie(P, pv)) = max(0, pointsDeVie(P) - pv)
		post = pointsDeVie() == Math.max(0, pv_pre - pv);
		if(!post) {
			throw new PostconditionError("pointsDeVie(retirerPointsDeVie(P, pv)) = max(0, pointsDeVie(P) - pv)");
		}
//		post estPorte(retirerPointsDeVie(P, pv)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(retirerPointsDeVie(P, pv)) = estPorte(P)");
		}
//		post estJete(retirerPointsDeVie(P, pv)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(retirerPointsDeVie(P, pv)) = estJete(P)");
		}
//		post choseEquipee(retirerPointsDeVie(P, pv)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(retirerPointsDeVie(P, pv)) = choseEquipee(P)");
		}
//		post position(retirerPointsDeVie(P, pv)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(retirerPointsDeVie(P, pv)) = position(P)");
		}
//		post versLaDroite(retirerPointsDeVie(P, pv)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(retirerPointsDeVie(P, pv)) = versLaDroite(P)");
		}
//		post estGele(retirerPointsDeVie(P, pv)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(retirerPointsDeVie(P, pv)) = estGele(P)");
		}
	}

	@Override
	public void ramasser(Equipable e) throws ComposantError {
		boolean pre;
//		pre ramasser(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ !estEquipe(P) ^ estEquipable(E) ^ !estPorte(E)
		pre = !estVaincu() && estGele() == 0 && !estEquipe() && e.estEquipable() && !e.estPorte();
		if(!pre) {
			throw new PreconditionError("ramasser(P, O) require !estVaincu(P) ^ estGele(P) = 0 ^ !estEquipe(P) ^ estEquipable(E) ^ !estPorte(E)");
		}
		
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();
		
		checkInvariants();
		
		delegate().ramasser(e);
		
		checkInvariants();
		
		boolean post;
//		post choseEquipee(ramasser(P, E)) = E
		post = Toolbox.equals(choseEquipee(), e);
		if(!post) {
			throw new PostconditionError("choseEquipee(ramasser(P, E)) = E");
		}
//		post estPorte(ramasser(P, E)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(ramasser(P, E)) = estPorte(P)");
		}
//		post estJete(ramasser(P, E)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(ramasser(P, E)) = estJete(P)");
		}
//		post pointsDeVie(ramasser(P, E)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(ramasser(P, E)) = pointsDeVie(P)");
		}
//		post position(ramasser(P, E)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(ramasser(P, E)) = position(P))");
		}
//		post versLaDroite(ramasser(P, E)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(ramasser(P, E)) = versLaDroite(P)");
		}
//		post estGele(ramasser(P, E)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(ramasser(P, E)) = estGele(P)");
		}
	}

	@Override
	public void jeter() throws ComposantError {
		boolean pre;
//		pre jeter(P) require !estVaincu(P) ^ estGele(P) = 0 ^ estEquipe(P)
		pre = !estVaincu() && estGele() == 0 && estEquipe();
		if(!pre) {
			throw new PreconditionError("jeter(P) require !estVaincu(P) ^ estGele(P) = 0 ^ estEquipe(P)");
		}

		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();
		
		checkInvariants();
		
		delegate().jeter();
		
		checkInvariants();
		
		boolean post;
//		post choseEquipee(jeter(P)) = NULL
		post = choseEquipee() == null;
		if(!post) {
			throw new PostconditionError("choseEquipee(jeter(P)) = NULL");
		}
//		post estPorte(jeter(P)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(jeter(P)) = estPorte(P)");
		}
//		post estJete(jeter(P)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(jeter(P)) = estJete(P)");
		}
//		post pointsDeVie(jeter(P)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("choseEquipee(jeter(P)) = NULL");
		}
//		post position(jeter(P)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("position(jeter(P)) = position(P)");
		}
//		post versLaDroite(jeter(P)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(jeter(P)) = versLaDroite(P)");
		}
//		post estGele(jeter(P)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(jeter(P)) = estGele(P)");
		}
	}
	
	@Override
	public void deplacer(Position p) throws ComposantError {
		boolean pre;
//		pre deplacer(P, p) require !estVaincu(P) ^ estGele(P) = 0
		pre = !estVaincu() && estGele() == 0;
		if(!pre) {
			throw new PreconditionError("deplacer(P, p) require !estVaincu(P) ^ estGele(P) = 0");
		}
		
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		Equipable ce_pre = choseEquipee();
		int eg_pre = estGele();
		
		checkInvariants();
		
		delegate().deplacer(p);
		
		checkInvariants();
		
		boolean post;
//		post position(deplacer(P, p)) = p
		post = Toolbox.equals(position(), p);
		if(!post) {
			throw new PostconditionError("position(deplacer(P, p)) = p");
		}
//		post versLaDroite(deplacer(P, p)) = { true si Position::x(p) > Position::x(position(P))
//											{ false si Position::x(p) < Position::x(position(P))
//											{ versLaDroite(P) sinon
		if(p.x() > p_pre.x()) {
			post = versLaDroite() == true;
			if(!post) {
				throw new PostconditionError("Position::x(p) > Position::x(position(P)) -> versLaDroite(deplacer(P, p)) = true");
			}
		}
		else if(p.x() < p_pre.x()) {
			post = versLaDroite() == false;
			if(!post) {
				throw new PostconditionError("Position::x(p) < Position::x(position(P)) -> versLaDroite(deplacer(P, p)) = false");
			}
		}
		else {
			post = versLaDroite() == vld_pre;
			if(!post) {
				throw new PostconditionError("Position::x(p) = Position::x(position(P)) -> versLaDroite(deplacer(P, p)) = versLaDroite(P)");
			}
		}
//		post pointsDeVie(deplacer(P, p)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(deplacer(P, p)) = pointsDeVie(P)");
		}
//		post estPorte(deplacer(P, p)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(deplacer(P, p)) = estPorte(P)");
		}
//		post estJete(deplacer(P, p)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(deplacer(P, p)) = estJete(P)");
		}
//		post choseEquipee(deplacer(P, p)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(deplacer(P, p)) = choseEquipee(P)");
		}
//		post estGele(deplacer(P, p)) = estGele(P)
		post = estGele() == eg_pre;
		if(!post) {
			throw new PostconditionError("estGele(deplacer(P, p)) = estGele(P)");
		}
	}

	@Override
	public void geler(int g) throws ComposantError {
		boolean pre;
//		pre geler(P, g) require !estVaincu(P) ^ g > 0
		pre = !estVaincu() && g > 0;
		if(!pre) {
			throw new PreconditionError("geler(P, g) require !estVaincu(P) ^ g > 0");
		}
		
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		Equipable ce_pre = choseEquipee();

		checkInvariants();

		delegate().geler(g);

		checkInvariants();

		boolean post;
//		post estGele(geler(P, g)) = g
		post = estGele() == g;
		if(!post) {
			throw new PostconditionError("estGele(geler(P, g)) = g");
		}
//		post pointsDeVie(geler(P, g)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(geler(P, g)) = pointsDeVie(P)");
		}
//		post estPorte(geler(P, g)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(geler(P, g)) = estPorte(P)");
		}
//		post estJete(geler(P, g)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(geler(P, g)) = estJete(P)");
		}
//		post choseEquipee(geler(P, g)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(geler(P, g)) = choseEquipee(P)");
		}
//		post position(geler(P, g)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("pointsDeVie(geler(P, g)) = pointsDeVie(P)");
		}
//		post versLaDroite(geler(P, g)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(geler(P, g)) = versLaDroite(P)");
		}
	}

	@Override
	public void degeler() throws ComposantError {
		int pv_pre = pointsDeVie();
		boolean ep_pre = estPorte();
		int ej_pre = estJete();
		Position p_pre = position();
		boolean vld_pre = versLaDroite();
		int eg_pre = estGele();
		Equipable ce_pre = choseEquipee();
		
		checkInvariants();
		
		delegate().degeler();
		
		checkInvariants();
		
		boolean post;

//		post estGele(degeler(P)) = { max(0, estGele(P) - 1) si !estPorte(P)
//								   { estGele(P) sinon
		if(!estPorte()) {
			post = estGele() == Math.max(0,  eg_pre - 1);
			if(!post) {
				throw new PostconditionError("!estPorte(P) -> estGele(degeler(P)) = max(0, estGele(P) - 1)");
			}
		}
		else {
			post = estGele() == eg_pre;
			if(!post) {
				throw new PostconditionError("estPorte(P) -> estGele(degeler(P)) = estGele(P)");
			}
		}
//		post pointsDeVie(degeler(P)) = pointsDeVie(P)
		post = pointsDeVie() == pv_pre;
		if(!post) {
			throw new PostconditionError("pointsDeVie(degeler(P)) = pointsDeVie(P)");
		}
//		post estPorte(degeler(P)) = estPorte(P)
		post = estPorte() == ep_pre;
		if(!post) {
			throw new PostconditionError("estPorte(degeler(P)) = estPorte(P)");
		}
//		post estJete(degeler(P)) = estJete(P)
		post = estJete() == ej_pre;
		if(!post) {
			throw new PostconditionError("estJete(degeler(P)) = estJete(P)");
		}
//		post choseEquipee(degeler(P)) = choseEquipee(P)
		post = Toolbox.equals(choseEquipee(), ce_pre);
		if(!post) {
			throw new PostconditionError("choseEquipee(degeler(P)) = choseEquipee(P)");
		}
//		post position(degeler(P)) = position(P)
		post = Toolbox.equals(position(), p_pre);
		if(!post) {
			throw new PostconditionError("pointsDeVie(degeler(P)) = pointsDeVie(P)");
		}
//		post versLaDroite(degeler(P)) = versLaDroite(P)
		post = versLaDroite() == vld_pre;
		if(!post) {
			throw new PostconditionError("versLaDroite(degeler(P)) = versLaDroite(P)");
		}
	}
}
